module myexamples/sudoku

abstract sig Num { sudoku : Num one -> one Num }
abstract sig B1, B2, B3 extends Num {}

one sig N1, N2, N3 extends B1 {}
one sig N4, N5, N6 extends B2 {}
one sig N7, N8, N9 extends B3 {}

//abstract sig R1, R2 extends Num {}

//fact rows_onto { all x: Num | Num in sudoku[x,Num] }
fact columns_onto { all y: Num | Num in sudoku[Num,y] }

fact B1B1_onto { Num in sudoku[B1,B1] }
fact B1B2_onto { Num in sudoku[B1,B2] }
fact B1B3_onto { Num in sudoku[B1,B3] }
fact B2B1_onto { Num in sudoku[B2,B1] }
fact B2B2_onto { Num in sudoku[B2,B2] }
fact B2B3_onto { Num in sudoku[B2,B3] }
fact B3B1_onto { Num in sudoku[B3,B1] }
fact B3B2_onto { Num in sudoku[B3,B2] }
fact B3B3_onto { Num in sudoku[B3,B3] }

//Hieronder stelt dat er 4 vierkanten zijn die van rij2tm4 X kolom2tm4 zijn enz.
//Met het huidige problem is de sudoku niet op te lossen. 
//Ik vraag me ook af of het problem overeenkomt met de opgave die we gekregen hebben
fact test { Num in sudoku[N2 + N3 + N4, N2 + N3 + N4]}
fact test { Num in sudoku[N2 + N3 + N4, N6 + N7 + N8]}
fact test { Num in sudoku[N6 + N7 + N8, N2 + N3 + N4]}
fact test { Num in sudoku[N6 + N7 + N8, N6 + N7 + N8]}

assert rows_onto { all x: Num | Num in sudoku[x,Num] }
//check rows_onto


fact problem {
N1->N5 + N2->N3 + N5->N7 in sudoku[N1]
N1->N6 + N4->N1 + N5->N9 + N6->N5 in sudoku[N2]
N2->N9 + N3->N8 + N8->N6 in sudoku[N3]
N1->N8 + N5->N6 + N9->N3 in sudoku[N4]
N1->N4 + N4->N8 + N6->N3 + N9->N1 in sudoku[N5]
N1->N7 + N5->N2 + N9->N6 in sudoku[N6]
N2->N6 + N7->N2 + N8->N8 in sudoku[N7]
N4->N4 + N5->N1 + N6->N9 + N9->N5 in sudoku[N8]
N5->N8 + N8->N7 + N9->N9 in sudoku[N9]
}
pred show () {}
run show
